Inference at * 1 1 1 1 
Iof proof for Lemma nat ind tp:

.....downcase..... NILNIL

1. P : {k}
2. P(0)
3. i:. P(i - 1)  P(i)
4. i : 
5. i < 0
6. ((i + 1)  0 )  P(i + 1)
  (i  0 )  P(i) 

latex

 by D 0 

latex

 1: 

 1: 7. i  0 
 1:   P(i)
 2: .....wf..... NILNIL

 2:   (i  0 )  
 .

Definitions	P  Q, t  T,
Lemmas	ge wf